This paper presents our approach to the quantitative modeling and analysis ofhighly (re)configurable systems, such as software product lines. Differentcombinations of the optional features of such a system give rise tocombinatorially many individual system variants. We use a formal modelinglanguage that allows us to model systems with probabilistic behavior, possiblysubject to quantitative feature constraints, and able to dynamically install,remove or replace features. More precisely, our models are defined in theprobabilistic feature-oriented language QFLAN, a rich domain specific language(DSL) for systems with variability defined in terms of features. QFLANspecifications are automatically encoded in terms of a process algebra whoseoperational behavior interacts with a store of constraints, and hence allows toseparate system configuration from system behavior. The resulting probabilisticconfigurations and behavior converge seamlessly in a semantics based ondiscrete-time Markov chains, thus enabling quantitative analysis. Our analysisis based on statistical model checking techniques, which allow us to scale tolarger models with respect to precise probabilistic analysis techniques. Theanalyses we can conduct range from the likelihood of specific behavior to theexpected average cost, in terms of feature attributes, of specific systemvariants. Our approach is supported by a novel Eclipse-based tool whichincludes state-of-the-art DSL utilities for QFLAN based on the Xtext frameworkas well as analysis plug-ins to seamlessly run statistical model checkinganalyses. We provide a number of case studies that have driven and validatedthe development of our framework.
展开▼
